COMMENT |
  The syntax for this command is:
  CIRCUMSCRIBE NAME < ... <predsym> <predpar> <varlist> ... > IN <vl>;
  The result is to produce an axiom 
  Below is a working example 
  This is now on the system. |

DECLARE INDVAR x;
DECLARE INDCONST a b;
DECLARE PREDCONST isblock 1;
DECLARE PREDPAR P 1;

AXIOM twoblocks:	isblock(a)∧isblock(b);;

CIRCUMSCRIBE newaxiom isblock P x IN twoblocks;

Circumscription has produced the following new axiom:
newaxiom: ((P(a)∧P(b))∧∀x.(P(x)⊃isblock(x)))⊃∀x.(isblock(x)⊃P(x));;

∧I newaxiom[P←λx.(x=a∨x=b)];

1 (((a=a∨a=b)∧(b=a∨b=b))∧∀x.((x=a∨x=b)⊃isblock(x)))⊃∀x.(isblock(x)⊃(x=a∨x=b))  

tauteq 1:#1#2#1 twoblocks;

2 (x=a∨x=b)⊃isblock(x)  

∀i 2 x;

3 ∀x.((x=a∨x=b)⊃isblock(x))  

tauteq 1:#2 1 3;

4 ∀x.(isblock(x)⊃(x=a∨x=b))  

∀e 4 x;

5 isblock(x)⊃(x=a∨x=b)  

tauteq isblock(x)≡(x=a∨x=b) 5 twoblocks;

6 isblock(x)≡(x=a∨x=b)  

∀i 6 x;

7 ∀x.(isblock(x)≡(x=a∨x=b))  

show axioms;

newaxiom: ((P(a)∧P(b))∧∀x.(P(x)⊃isblock(x)))⊃∀x.(isblock(x)⊃P(x))
twoblocks: isblock(a)∧isblock(b)